\documentclass{article}


\usepackage{amssymb}
\usepackage{amsthm}

\usepackage{relsize}
\usepackage{amsmath}
\usepackage{url}
\usepackage{listings}
\usepackage[ruled]{algorithm} %
\usepackage[noend]{algorithmic} %
\renewcommand\algorithmiccomment[1]{// \textit{#1}} %
\usepackage{microtype}
\usepackage{pslatex}
\usepackage{xspace}
\usepackage{yglabels}
\usepackage{yglang}
\usepackage{ygequation}
\usepackage{graphicx}

\newcommand{\formalrule}[1]{\mbox{\textsc{\scriptsize #1}}}
\newcommand{\myrule}[1]{\textsc{\codesmaller #1 Rule}}
\newcommand{\umyrule}[1]{\textbf{\underline{\textsc{\codesmaller #1 Rule}}}}

\newcommand{\normalcode}[1]{\texttt{\textup{#1}}}
\def\codesmaller{\small}
\newcommand{\myCOMMENT}[1]{\COMMENT{\small #1}}
\newcommand{\code}[1]{\texttt{\textup{\codesmaller #1}}}

\newcommand{\smallcode}[1]{\texttt{\textup{\scriptsize #1}}}

\newcommand{\keyword}[1]{\code{#1}}

\newcommand{\hparen}[1]{\code{(}#1\code{)}}

\newcommand{\hgn}[1]{\lt#1\gt} %

\newcommand{\Own}{{\it O}}
\newcommand{\Ifn}[1]{\ensuremath{I(#1)}}
\newcommand{\Ofn}[1]{\ensuremath{O(#1)}}
\newcommand{\Cooker}[1]{\ensuremath{{\kappa}(#1)}}
\newcommand{\Owner}[1]{\ensuremath{{\theta}(#1)}}
\newcommand{\Oprec}[0]{\ensuremath{\preceq_{\theta}}}
\newcommand{\Tprec}[0]{\ensuremath{\preceq^T}}
\newcommand{\TprecNotEqual}[0]{\ensuremath{\prec^T}}
\newcommand{\OprecNotEqual}[0]{\ensuremath{\prec_{\theta}}}
\newcommand{\IfnDelta}[1]{\ensuremath{I_\Delta(#1)}}
\newcommand\Abs[1]{\ensuremath{\left\lvert#1\right\rvert}}
\newcommand{\erase}[1]{\ensuremath{\Abs{#1}}}

\newcommand{\CookerH}[1]{\ensuremath{{\kappa}_H(#1)}}
\newcommand{\IfnH}[1]{\ensuremath{I_H(#1)}}
\newcommand{\OwnerH}[1]{\ensuremath{{\theta}_H(#1)}}
\newcommand{\KGdash}[0]{\ensuremath{K,\Gamma \vdash }}
\newcommand{\reducesto}[0]{\rightarrow}

\usepackage{color}
\definecolor{light}{gray}{.75}

\newcommand{\todo}[1]{\textbf{[[#1]]}}

\newcommand{\TODO}[1]{\todo{TODO: #1}}

\newcommand\xX[1]{$\textsuperscript{\textit{\text{#1}}}$}

\newcommand{\ol}[1]{\overline{#1}}
\newcommand{\nounderline}[1]{{#1}}

\newcommand{\typerule}[2]{
\begin{array}{c}
  #1 \\
\hline
  #2
\end{array}}

\newcommand{\inside}{\prec}
\newcommand{\visible}{{\it visible}}
\newcommand{\placeholderowners}{{\it placeholderowners}}
\newcommand{\nullexpression}{{\tt null}}
\newcommand{\errorexpression}{{\tt error}}
\newcommand{\locations}{{\it locations}} %
\newcommand{\xo}{{\tt X^O}}
\newcommand{\no}{{\tt N^O}}
\newcommand{\co}{{\tt C^O}}
\newcommand{\I}{\it I}

\newcommand\mynewcommand[2]{\newcommand{#1}{#2\xspace}}

\mynewcommand{\hA}{\code{A}} %
\mynewcommand{\hB}{\code{B}} %

\mynewcommand{\hI}{\code{I}} %

\mynewcommand{\hJ}{\code{J}}
\mynewcommand{\hO}{\code{O}}
\mynewcommand{\ho}{\code{o}}

\mynewcommand{\hX}{\code{X}} %
\mynewcommand{\hY}{\code{Y}} %
\mynewcommand{\hC}{\code{C}} %
\mynewcommand{\hc}{\code{c}} %
\mynewcommand{\hL}{\code{L}} %
\mynewcommand{\hM}{\code{M}} %
\mynewcommand{\hN}{\code{N}} %
\mynewcommand{\hm}{\code{m}} %
\mynewcommand{\he}{\code{e}} %
\mynewcommand{\hv}{\code{v}} %
\mynewcommand{\hl}{\code{l}} %
\mynewcommand{\lroot}{\code{l}_\top} %
\mynewcommand{\lthis}{\code{l}_\smallcode{this}} %
\mynewcommand{\hx}{\code{x}} %
\mynewcommand{\hf}{\code{f}} %
\mynewcommand{\hF}{\code{F}} %
\mynewcommand{\hT}{\code{T}} %
\mynewcommand{\hU}{\code{U}} %
\mynewcommand{\hV}{\code{V}} %
\mynewcommand{\hH}{\code{H}} %
\mynewcommand{\hS}{\code{S}}
\mynewcommand{\hsub}{\code{/}} %
\mynewcommand{\hthis}{\code{this}} %
\mynewcommand{\hclass}{\code{class}}
\mynewcommand{\hreturn}{\code{return}}
\mynewcommand{\hnew}{\code{new}}
\newcommand{\lt}{\code{<}}%
\newcommand{\gt}{\code{>}}%

\mynewcommand{\this}{\keyword{this}}
\mynewcommand{\Object}{\code{Object}}
\mynewcommand{\const}{\keyword{const}} %
\mynewcommand{\mutable}{\keyword{mutable}} %
\mynewcommand{\romaybe}{\keyword{romaybe}} %

\newtheorem{theorem}{Theorem}[section]
\newtheorem{definition}[theorem]{Definition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{fact}[theorem]{Fact}
\newtheorem{example}[theorem]{Example}
\newtheorem{remark}[theorem]{Remark}

\mynewcommand{\IP}{\code{I}}   %
\mynewcommand{\JP}{\code{J}}   %

\mynewcommand{\Iparam}{Immutability parameter}
\mynewcommand{\iparam}{immutability parameter}
\mynewcommand{\iparams}{immutability parameters}
\mynewcommand{\Iparams}{Immutability parameters}
\mynewcommand{\Iarg}{Immutability argument}
\mynewcommand{\iarg}{immutability argument}
\mynewcommand{\iargs}{immutability arguments}
\mynewcommand{\Iargs}{Immutability arguments}
\mynewcommand{\ReadOnly}{\code{ReadOnly}}
\mynewcommand{\WriteOnly}{\code{WriteOnly}}
\mynewcommand{\None}{\code{None}}
\mynewcommand{\Mutable}{\code{Mutable}}
\mynewcommand{\Immut}{\code{Immut}}
\mynewcommand{\Raw}{\code{Raw}}

\mynewcommand{\This}{\code{This}}
\mynewcommand{\World}{\code{World}}

\mynewcommand{\OMutable}{\code{@OMutable}}
\mynewcommand{\OI}{\code{@OI}}

\mynewcommand{\InVariantAnnot}{\code{@InVariant}}

\newcommand{\func}[1]{\text{\textnormal{\textit{\codesmaller #1}}}}

\mynewcommand{\st}{\ensuremath{\mathrel{{\leq}}}} %
\mynewcommand{\notst}{\mathrel{\st\hspace{-1.5ex}\rule[-.25em]{.4pt}{1em}~}}
\mynewcommand{\tl}{\ensuremath{\triangleleft}}
\mynewcommand{\gap}{~ ~ ~ ~ ~ ~}

\newcommand{\RULE}[1]{\textsc{\scriptsize{}#1}} %

\mynewcommand{\DA}{\texttt{DA}}
\mynewcommand{\ok}{\texttt{OK}}
\mynewcommand{\subterm}{\func{subterm}}
\mynewcommand{\TP}{\func{TP}} %
\mynewcommand{\CT}{\func{CT}} %
\mynewcommand{\mtype}{\func{mtype}}
\mynewcommand{\mbody}{\func{mbody}}
\mynewcommand{\bound}{\func{bound}_\Delta}
\mynewcommand{\substitute}{\func{substitute}}
\mynewcommand{\fields}{\func{fields}}
\mynewcommand{\ftype}{\func{ftype}}
\mynewcommand{\mguard}{\func{mguard}}
\mynewcommand{\isTransitive}{\func{isTransitive}}
\DeclareMathOperator{\dom}{dom}

\mynewcommand\xth{\xX{th}}
\mynewcommand\xrd{\xX{rd}}
\mynewcommand\xnd{\xX{nd}}
\mynewcommand\xst{\xX{st}}
\mynewcommand\ith{$i$\xth}
\mynewcommand\jth{$j$\xth}

\mynewcommand{\myindent}{~~}

\makeatletter
\def\topfigrule{\kern3\p@ \hrule \kern -3.4\p@} %
\def\botfigrule{\kern-3\p@ \hrule \kern 2.6\p@} %
\def\dblfigrule{\kern3\p@ \hrule \kern -3.4\p@} %
\makeatother

\setlength{\textfloatsep}{.75\textfloatsep}

\makeatletter
\makeatother

\usepackage{bold-extra}

\newcommand{\ttlcb}{\texttt{\char "7B}}
\newcommand{\ttrcb}{\texttt{\char "7D}}
\newcommand{\lb}{\ttlcb}
\newcommand{\rb}{\ttrcb}

\setlength{\leftmargini}{.75\leftmargini}

\lstset{language=java,basicstyle=\ttfamily\small}


\author{Alex Potanin, Yoav Zibin, Michael D. Ernst}

% Mahmood Ali, Paley Li

\title{Ownership, Immutability, and Generic Types}

\begin{document}

\maketitle

\begin{abstract}
The Java language lacks the important notions of \textit{ownership} (an object owns its representation to prevent unwanted aliasing) and \textit{immutability} (the division into mutable, immutable, and readonly data and references). Programmers are prone to design errors, such as representation exposure or violation of immutability contracts. This paper presents \textit{Ownership Immutability Generic Java} (OIGJ), a backward-compatible purely-static language extension supporting ownership and immutability. We formally defined a core calculus for OIGJ, based on Featherweight Java, and proved it sound. We also implemented OIGJ and performed case studies on 33,000 lines of code.

Creation of immutable cyclic structures requires a ``\textit{cooking phase}'' in which the structure is mutated but the outside world cannot observe this mutation. OIGJ uses \textit{ownership} information to facilitate creation of \textit{immutable} cyclic structures, by safely prolonging the cooking phase even after the constructor finishes.

OIGJ is easy for a programmer to use, and it is easy to implement (flow-insensitive, adding only 14 rules to those of Java). Yet, OIGJ is more expressive than previous ownership languages, in the sense that it can type-check more good code. OIGJ can express the factory and visitor patterns, and
OIGJ can type-check Sun's \texttt{java.util} collections (except for the \texttt{clone} method) without refactoring and with only a small number of annotations. Previous work required major refactoring of existing code in order to fit its ownership restrictions. Forcing refactoring of well-designed code is undesirable because it costs programmer effort, degrades the design, and hinders adoption in the mainstream community.
\end{abstract}


\Section[introduction]{Introduction}
\input{introduction}

\paragraph{Contributions}
\input{contributions}


\Section[oigj-language]{OIGJ Language}
\input{oigj-language}


\Section[formal]{Formalization and Type Soundness}
\input{formal}


\Section[case-studies]{OIGJ Case Studies}
\input{case-studies}


\Section[related-work]{Related Work}
\input{related-work}


\Section[conclusion]{Conclusion}
\input{conclusions}


\section*{Acknowledgements}


This work was supported by the grants from RSNZ Marsden,
ISAT, and NSF CNS-0855252. We especially thank
Werner Dietl, James Noble, ELVIS, and the
anonymous referees.


\Section[proofs]{Proofs}
\input{proofs}


\bibliographystyle{plain}
\bibliography{extra,bibstring-abbrev,types,alias,ernst,invariants,pag}


\end{document}
